; EXPECT: sat
(set-logic ALL)
(set-option :incremental false)
(declare-fun a0 () Bool)
(declare-fun a1 () Bool)
(declare-fun a2 () Bool)
(declare-fun a3 () Bool)
(declare-fun a4 () Bool)
(declare-fun a5 () Bool)
(declare-fun a6 () Bool)
(declare-fun a7 () Bool)
(declare-fun a8 () Bool)
(declare-fun a9 () Bool)
(assert a5)
(assert (or a0 (and a1 (or a2 (and a3 (and a4 (and a5 (and true (and a3 (and a6 (and a7 (and a8 a9))))))))))))
(check-sat)
